<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN"
"http://www.w3.org/TR/html4/loose.dtd">

<html>
<head>

<title>
PRISM Manual | ConfiguringPRISM / ComputationEngines 
</title>

<meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
<meta name="keywords" content="prism, probabilistic, symbolic, model, checker, verification, birmingham, oxford, parker, norman, kwiatkowska">

<link rel="icon" href="../pub/skins/offline/images/p16.ico" type="image/x-icon">
<link rel="shortcut icon" href="../pub/skins/offline/images/p16.ico" type="image/x-icon">

<!--HTMLHeader--><style type='text/css'><!--
  ul, ol, pre, dl, p { margin-top:0px; margin-bottom:0px; }
  code.escaped { white-space: nowrap; }
  .vspace { margin-top:1.33em; }
  .indent { margin-left:40px; }
  .outdent { margin-left:40px; text-indent:-40px; }
  a.createlinktext { text-decoration:none; border-bottom:1px dotted gray; }
  a.createlink { text-decoration:none; position:relative; top:-0.5em;
    font-weight:bold; font-size:smaller; border-bottom:none; }
  img { border:0px; }
  .editconflict { color:green; 
  font-style:italic; margin-top:1.33em; margin-bottom:1.33em; }

  table.markup { border:2px dotted #ccf; width:90%; }
  td.markup1, td.markup2 { padding-left:10px; padding-right:10px; }
  table.vert td.markup1 { border-bottom:1px solid #ccf; }
  table.horiz td.markup1 { width:23em; border-right:1px solid #ccf; }
  table.markup caption { text-align:left; }
  div.faq p, div.faq pre { margin-left:2em; }
  div.faq p.question { margin:1em 0 0.75em 0; font-weight:bold; }
  div.faqtoc div.faq * { display:none; }
  div.faqtoc div.faq p.question 
    { display:block; font-weight:normal; margin:0.5em 0 0.5em 20px; line-height:normal; }
  div.faqtoc div.faq p.question * { display:inline; }
   
    .frame 
      { border:1px solid #cccccc; padding:4px; background-color:#f9f9f9; }
    .lfloat { float:left; margin-right:0.5em; }
    .rfloat { float:right; margin-left:0.5em; }
a.varlink { text-decoration:none; }

.sourceblocklink {
  text-align: right;
  font-size: smaller;
}
.sourceblocktext {
  padding: 0.5em;
  border: 1px solid #808080;
  color: #000000;
  background-color: #f1f0ed;
}
.sourceblocktext div {
  font-family: monospace;
  font-size: small;
  line-height: 1;
  height: 1%;
}
.sourceblocktext div.head,
.sourceblocktext div.foot {
  font: italic medium serif;
  padding: 0.5em;
}

--></style>  <meta name='robots' content='index,follow' />


<link type="text/css" rel="stylesheet" href="../pub/skins/offline/css/base.css">
<link type="text/css" rel="stylesheet" href="../pub/skins/offline/css/prism.css">
<link type="text/css" rel="stylesheet" href="../pub/skins/offline/css/prismmanual.css">

</head>

<body text="#000000" bgcolor="#ffffff">

<div id="layout-maincontainer">
<div id="layout-main">

<div id="prism-mainbox">

<!-- ============================================================================= -->

<!--PageHeaderFmt-->
<!--/PageHeaderFmt-->

<!--PageTitleFmt-->
  <div id="prism-man-title">
    <p><a class='wikilink' href='Introduction.html'>Configuring PRISM</a> /
</p><h1>Computation Engines</h1>

  </div>
<!--PageText-->
<div id='wikitext'>
<h3>Computation engines</h3>
<p>An important feature of the tool is its <em>engines</em>.
PRISM is primarily a <em>symbolic</em> model checker: its basic underlying data structures are binary decision diagrams (BDDs) and multi-terminal BDDs (MTBDDs).
When performing numerical computation on DTMCs, MDPs and CTMCs, however, the tool can use one of three engines.
The first is implemented purely in <em>MTBDDs</em> (and BDDs); the second uses <em>sparse matrices</em>;
and the third is a <em>hybrid</em>, using a combination of the other two.
</p>
<p class='vspace'>The choice of engine ("MTBDD", "sparse" or "hybrid") should not affect the results of model checking - all engines perform essentially the same calculations. In some cases, though, certain functionality is not available with all engines and PRISM will either automatically switch to an appropriate engine, or prompt you yo do so.
Performance (time and space), however, may vary significantly and if you are using too much time/memory with one engine, it may be worth experimenting. Below, we briefly summarise the key characteristics of each engine.
</p>
<div class='vspace'></div><ul><li>The <strong>hybrid</strong> engine is enabled by default in PRISM. It uses a combination of <em>symbolic</em> and <em>explicit</em> data structures (as used in the MTBDD and sparse engines, respectively). In general it provides the best compromise between time and memory usage: it (almost) always uses less memory than the sparse engine, but is typically slightly slower. The size of model which can be handled with this engine is quite predictable. The limiting factor in terms of memory usage comes from the storage of 2-4 (depending on the computation being performed) arrays of 8-byte values, one for each state in the model. So, a typical PC can handle models with between 10<sup>7</sup> and 10<sup>8</sup> states (one vector for 10<sup>7</sup> states uses approximately 75 MB).
<div class='vspace'></div></li><li>The <strong>sparse</strong> engine can be a good option for smaller models where model checking takes a long time. For larger models, however, memory usage quickly becomes prohibitive. As a rule of thumb, the upper limit for this engine, in terms of model sizes which can be handled, is about a factor of 10 less than the hybrid engine.
<div class='vspace'></div></li><li>The <strong>MTBDD</strong> engine is much more unpredictable in terms of performance but, when a model exhibits a lot of structure and regularity, can be very effective. This engine has been successfully applied to extremely large structured (but non-trivial) models, in cases where the other two engines cannot be applied. The MTBDD engine often performs poorly when the model (or solutions computed from it) contain lots of distinct probabilities/rates; it performs best when there are few such values. For this reason the engine is often successfully applied to MDP models, but much less frequently to CTMCs. When using the MTBDD engine, the <em>variable ordering</em> of your model is especially important. This topic is covered in the <a class='wikilink' href='../FrequentlyAskedQuestions/PRISMModelling.html#ordering'>FAQ</a> section.
</li></ul><p class='vspace'>When using the PRISM GUI, the engine to be used for model checking can be selected from the "Engine" option under the "PRISM" tab of the "Options" dialog. From the command-line, engines are activated using the <code>-mtbdd</code>, <code>-sparse</code> and <code>-hybrid</code> (or <code>-m</code>, <code>-s</code> and <code>-h</code>, respectively) switches, e.g.:
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock1'>
  <div class='sourceblocktext'><div class="shell"><span style="font-weight:bold;">prism poll2.sm -tr 1000 -s</span><br/>
</div></div>
  <div class='sourceblocklink'><a href='ComputationEngines@action=sourceblock&amp;num=1' type='text/plain'>[&#036;[Get Code]]</a></div>
</div>

<p class='vspace'>For further information and technical details about PRISM's implementation and engines, see: [<a class='wikilink' href='../Main/References.html#Par02'>Par02</a>],[<a class='wikilink' href='../Main/References.html#KNP04b'>KNP04b</a>].
</p>
<p class='vspace'>Note also that precise details regarding the memory usage of the current engine are displayed during model checking (from the GUI, check the "Log" tab). This can provide valuable feedback when experimenting with different engines.
</p>
<p class='vspace'><a name='pta' id='pta'></a>
</p><h3>PTA Engines</h3>
<p>The techniques used to model check PTAs are different to the ones used for DTMCs, MDPs and CTMCs. For PTAs, PRISM currently has two distinct engines that can be used:
</p>
<div class='vspace'></div><ul><li>The <strong>stochastic games</strong> engine uses abstraction-refinement techniques based on stochastic two-player games [<a class='wikilink' href='../Main/References.html#KNP09c'>KNP09c</a>].
<div class='vspace'></div></li><li>The <strong>digital clocks</strong> engine performs a discretisation, in the form of a language-level model translation, that reduces the problem to one of model checking over a finite-state MDP [<a class='wikilink' href='../Main/References.html#KNPS06'>KNPS06</a>].
</li></ul><p class='vspace'>The default engine for PTAs is "stochastic games" because it generally scales better [<a class='wikilink' href='../Main/References.html#KNP09c'>KNP09c</a>]. The engine to be used can be specified using the "PTA model checking method" setting in the "PRISM" options panel in the GUI. From the command-line, switch <code>-ptamethod &lt;name&gt;</code> should be used where <code>&lt;name&gt;</code> is either <code>games</code> or <code>digital</code>.
</p>
<p class='vspace'>The choice of engine for PTA model checking affects restrictions that imposed on both
the <a class='wikilink' href='../ThePRISMLanguage/PTAs.html'>modelling language</a>
and the types of <a class='wikilink' href='../PropertySpecification/PTAProperties.html'>properties</a> that can be checked.
</p>
</div>


<!--PageFooterFmt-->
  <div id='prism-man-footer'>
  </div>
<!--/PageFooterFmt-->


<!-- ============================================================================= -->

</div> <!-- id="prism-mainbox" -->

</div> <!-- id="layout-main" -->
</div> <!-- id="layout-maincontainer" -->

<div id="layout-leftcol">
<div id="prism-navbar2">

<h3><a class='wikilink' href='../Main/Welcome.html'>PRISM Manual</a></h3>
<p><strong><a class='wikilink' href='Introduction.html'>Configuring PRISM</a></strong>
</p><ul><li><a class='wikilink' href='Introduction.html'>Introduction</a>
</li><li><a class='selflink' href='ComputationEngines.html'>Computation Engines</a>
</li><li><a class='wikilink' href='IterativeNumericalMethods.html'>Iterative Numerical Methods</a>
</li><li><a class='wikilink' href='OtherOptions.html'>Other Options</a>
</li></ul><p>[ <a class='wikilink' href='AllOnOnePage.html'>View all</a> ]
</p>


</div>  <!-- id="prism-navbar2" -->
</div> <!-- id="layout-leftcol" -->

</body>
</html>
